Definitions | {x:A| B(x)} , ||as||, i j , if b then t else f fi , left + right, Unit, i z j, i <z j, p  q, p  q, p   q, [d] , a < b, x f y, f(a), a < b, null(as), x =a y, P   Q, P & Q, x:A B(x), P  Q, tt,  b, , ff, , , (i = j), n+m, #$n, l[i], b, x:A. B(x), x:A B(x), t T, A, s = t, {i..j }, type List, Type, a < b |